\begin{tabbing}
SESAxioms\=\{i:l\}\+
\\[0ex]($E$; $T$; ${\it pred?}$; ${\it info}$; ${\it when}$; ${\it after}$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(\=$\forall$$e$:$E$, $l$:IdLnk.\+\+
\\[0ex]$\exists$${\it e'}$:$E$.
\\[0ex]$\forall$${\it e''}$:$E$.
\\[0ex]rcv?(${\it info}$;${\it e''}$)
\\[0ex]$\Rightarrow$ sender(${\it info}$;${\it e''}$) $=$ $e$ $\in$ $E$
\\[0ex]$\Rightarrow$ link(${\it info}$;${\it e''}$) $=$ $l$ $\in$ IdLnk
\\[0ex]$\Rightarrow$ ${\it e''}$ $=$ ${\it e'}$ $\in$ $E$ $\vee$ cless($E$;${\it pred?}$;${\it info}$;${\it e''}$;${\it e'}$) \& loc(${\it info}$;${\it e'}$) $=$ destination($l$) $\in$ Id)
\-\\[0ex]\& \=(\=$\forall$$e$:$E$, ${\it e'}$:$E$.\+\+
\\[0ex]loc(${\it info}$;$e$) $=$ loc(${\it info}$;${\it e'}$) $\in$ Id $\Rightarrow$ ${\it pred?}$($e$) $=$ ${\it pred?}$(${\it e'}$) $\in$ $E$+Unit $\Rightarrow$ $e$ $=$ ${\it e'}$ $\in$ $E$)
\-\\[0ex]\& strongwellfounded($E$; $e$,${\it e'}$.pred!($E$;${\it pred?}$;${\it info}$;$e$;${\it e'}$))
\\[0ex]\& ($\forall$$e$:$E$. $\neg$first(${\it pred?}$;$e$) $\Rightarrow$ loc(${\it info}$;pred(${\it pred?}$;$e$)) $=$ loc(${\it info}$;$e$) $\in$ Id)
\\[0ex]\& ($\forall$$e$:$E$. rcv?(${\it info}$;$e$) $\Rightarrow$ loc(${\it info}$;sender(${\it info}$;$e$)) $=$ source(link(${\it info}$;$e$)) $\in$ Id)
\\[0ex]\& (\=$\forall$$e$:$E$, ${\it e'}$:$E$.\+
\\[0ex]rcv?(${\it info}$;$e$)
\\[0ex]$\Rightarrow$ rcv?(${\it info}$;${\it e'}$)
\\[0ex]$\Rightarrow$ link(${\it info}$;$e$) $=$ link(${\it info}$;${\it e'}$) $\in$ IdLnk
\\[0ex]$\Rightarrow$ cless($E$;${\it pred?}$;${\it info}$;sender(${\it info}$;$e$);sender(${\it info}$;${\it e'}$))
\\[0ex]$\Rightarrow$ cless($E$;${\it pred?}$;${\it info}$;$e$;${\it e'}$))
\-\\[0ex]\& (\=$\forall$$e$:$E$.\+
\\[0ex]$\neg$first(${\it pred?}$;$e$)
\\[0ex]$\Rightarrow$ ($\forall$$x$:Id. ${\it when}$($x$,$e$) $=$ ${\it after}$($x$,pred(${\it pred?}$;$e$)) $\in$ $T$(loc(${\it info}$;$e$),$x$)))
\-\-\-
\end{tabbing}